ma{-}interface{-}val(${\it es}$;$X$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$let ${\it ds}$,$F$ = $X$(loc($e$)) in let $V$,$f$ = $F$(kind($e$)) in $f$((state when $e$),val($e$))